M:MsgA, l:IdLnk, tg:Id. rcv(l,tg) declared in M   

latex

Definitions	x:A. B(x), t  T, , rcv(l,tg) declared in M, t.1, t.2, x. t(x), MsgA, x(s)
Lemmas	assert wf, fpf-dom wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, rcv wf, Id wf, IdLnk wf, msga wf